(declare-fun v1 () Bool)
(declare-fun v4 () Bool)
(declare-fun v5 () Bool)
(declare-fun i2 () Int)
(declare-fun i4 () Int)
(declare-fun i5 () Int)
(declare-fun str0 () String)
(declare-fun str2 () String)
(declare-fun str3 () String)
(assert (= (= true true true (<= i4 i4 (- i5) (* i5 20 i2 i4) 0) true (= str0 str0 str0 str3 (str.substr str2 (* i5 20 i2 i4) (str.to_int str2))) v1) v1 (=> v5 v4) v5))
(check-sat)
